/**
 * Copyright (c) 2010-2011 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.logging.Logger;

import org.eclipse.jdt.core.dom.ASTNode;
import org.eclipse.jdt.core.dom.ASTVisitor;
import org.eclipse.jdt.core.dom.CompilationUnit;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.IMethodBinding;
import org.eclipse.jdt.core.dom.ISpecLoopStatement;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.Modifier;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.SingleVariableDeclaration;
import org.eclipse.jdt.core.dom.SpecCase;
import org.eclipse.jdt.core.dom.SpecCaseBody;
import org.eclipse.jdt.core.dom.SpecClause;
import org.eclipse.jdt.core.dom.SpecMethodDeclaration;
import org.eclipse.jdt.core.dom.SpecMethodSpecification;
import org.eclipse.jdt.core.dom.SpecTypeDeclaration;
import org.eclipse.jdt.core.dom.Statement;
import org.eclipse.jdt.core.dom.ThisExpression;
import org.eclipse.jdt.core.dom.TypeDeclaration;
import org.eclipse.jdt.core.dom.InfixExpression.Operator;
import org.eclipse.jdt.core.dom.SpecCase.Behavior;

import com.googlecode.syper.javasyp.checker.ExpressionEncoder.Lookup;
import com.googlecode.syper.javasyp.formulae.Field;
import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.formulae.Infix;
import com.googlecode.syper.javasyp.formulae.Literal;
import com.googlecode.syper.javasyp.formulae.Local;
import com.googlecode.syper.javasyp.formulae.Pre;
import com.googlecode.syper.javasyp.formulae.Prefix;
import com.googlecode.syper.javasyp.formulae.Ref;
import com.googlecode.syper.javasyp.formulae.Select;

import edu.cmu.cs.crystal.annotations.AnnotationSummary;

/**
 * @author kevin
 * @since Feb 13, 2011
 */
public class JmlContractRegistry extends ContractRegistry {

	private static final Logger logger = Logger.getLogger(JmlContractRegistry.class.getName());

	@Override
	protected Contract createContract(MethodDeclaration decl) {
		if (decl instanceof SpecMethodDeclaration)
			return createContract((SpecMethodDeclaration) decl);
		return super.createContract(decl);
	}

	@SuppressWarnings("unchecked")
	private Contract createContract(SpecMethodDeclaration decl) {
		SpecMethodSpecification spec = decl.getSpec();
		if (spec.isExtending())
			throw new UnsupportedOperationException("implement contract extension");
		if (spec.getSpecCases().length == 0)
			return super.createContract(decl);
		// TODO get superclass / interface contracts

		Contract result = new Contract();
		Map<String, Set<IVariableBinding>> modified =
			new LinkedHashMap<String, Set<IVariableBinding>>();

		IMethodBinding method = decl.resolveBinding();
		if (! decl.isConstructor() && ! Modifier.isStatic(decl.getModifiers())) {
			AnnotationSummary summ = annos.getSummaryForMethod(method);
			modified.put(Contract.THIS_VAR_NAME, getModified(
					summ.getReturn(), method.getDeclaringClass()));
		}

		for (SingleVariableDeclaration param : (List<SingleVariableDeclaration>) decl.parameters()) {
			result.addParam(param.getName().getIdentifier());
			IVariableBinding pBinding = param.resolveBinding();
			modified.put(param.getName().getIdentifier(),
					getModified(annos.getAnnosForVariable(pBinding), pBinding.getType()));
		}

		result.setModified(Collections.unmodifiableMap(modified));

		populateContract(new JmlContractLookup(decl), result, spec.getSpecCases());

		return result;
	}

	/**
	 * @param lookup
	 * @param contract
	 * @param cases specification cases to become part of the contract
	 */
	private void populateContract(Lookup lookup, Contract contract, SpecCase... cases) {
		Formula pre = null;
		Formula post = null;
		for (SpecCase c : cases) {
			SpecCaseBody body = c.getBody();
			if (body.getBodyCases() != null)
				throw new UnsupportedOperationException("implement body cases");

			Formula f = encode(lookup, body.getRequires(), SpecClause.Keyword.REQUIRES);
			if (pre == null)
				pre = f;
			else if (f != null)
				// disjunction of pre-conditions
				pre = Infix.toSynthetic(Operator.OR, pre, f);

			if (body.getBodyClauses() == null)
				continue;

			// TODO assignable and other clauses
			// TODO exceptional exits...
			Formula g = encode(lookup, body.getBodyClauses(), SpecClause.Keyword.ENSURES);
			if (Behavior.EXCEPTIONAL_BEHAVIOR == c.getKind()) {
				if (g != null)
					// TODO indicate a specification error...
					logger.warning("ensures clauses ignored in exceptional_behavior: " + c);
				// exceptional behavior has no normal return
				g = Literal.FALSE;
			}

			if (g == null)
				continue;
			else if (1 < cases.length && f != null)
				// make it pre ==> post if there are multiple cases
				g = Infix.toSynthetic(Operator.OR, Prefix.not(f), g);
			// conjunction of post-conditions
			post = (post == null) ? g : Infix.toSynthetic(Operator.CONDITIONAL_AND, post, g);
		}
		contract.setPre(pre);
		contract.setPost(post);
	}

	private Formula encode(Lookup lookup, SpecClause[] clauses, SpecClause.Keyword expected) {
		Formula result = null;
		for (SpecClause r : clauses) {
			if (r.isRedundant())
				continue; // ignore redundant specs
			if (expected != null & expected != r.getKeyword())
				throw new IllegalArgumentException("unexpected or unsupported clause: " + r.getKeyword());
			Formula f = JmlExpressionEncoder.encodeStandalone(r.getExpression(), lookup);
			result = result == null ? f : Infix.toSynthetic(Operator.CONDITIONAL_AND, result, f);
		}
		return result;
	}

	@Override
	public Collection<Expression> getLoopInvariant(Statement loopBody) {
		// include loop invariants declared with Pred.inv
		Collection<Expression> syperInvariant = super.getLoopInvariant(loopBody);

		ASTNode parent = loopBody.getParent();
		if (parent instanceof ISpecLoopStatement) {
			ISpecLoopStatement loopStmt = (ISpecLoopStatement) parent;
			if (loopStmt.getInvariants() != null && 0 < loopStmt.getInvariants().length) {
				ArrayList<Expression> result = new ArrayList<Expression>(loopStmt.getInvariants().length + syperInvariant.size());
				for (SpecClause c : loopStmt.getInvariants())
					// ignore redundant invariants
					if (!c.isRedundant())
						result.add(c.getExpression());
				result.addAll(syperInvariant);
				return result;
			}
		}
		return syperInvariant;
	}

	@Override
	public Collection<Expression> getInvariants(ITypeBinding type) {
		return collectInvariants(type, null);
	}

	@Override
	public Collection<Expression> getInvariants(TypeDeclaration type) {
		return collectInvariants(type.resolveBinding(), type);
	}

	private Collection<Expression> collectInvariants(ITypeBinding type, ASTNode hint) {
		Map<ITypeBinding, Collection<Expression>> holder =
			new LinkedHashMap<ITypeBinding, Collection<Expression>>();
		int size = collectInvariants(holder, type, hint);
		List<Expression> result = new ArrayList<Expression>(size);
		for (Collection<Expression> es : holder.values())
			result.addAll(es);
		return result;
	}

	private int collectInvariants(Map<ITypeBinding, Collection<Expression>> result, ITypeBinding type, ASTNode hint) {
		if (result.containsKey(type))
			// already processed (can happen with interfaces)
			return 0;
		TypeDeclaration typeSource = getTypeSource(type, hint);
		List<Expression> invs = extractInvariants(typeSource);
		result.put(type, invs);
		int size = invs.size();

		// now pile on supertype invariants
		if (typeSource != null)
			hint = typeSource;
		ITypeBinding supertype = type.getSuperclass();
		if (supertype != null)
			size += collectInvariants(result, supertype, hint);
		for (ITypeBinding i : type.getInterfaces())
			size += collectInvariants(result, i, hint);
		return size;
	}

	/**
	 * @param type
	 * @param hint
	 * @return
	 */
	private static TypeDeclaration getTypeSource(ITypeBinding type, ASTNode hint) {
		CompilationUnit root = getSource(type, hint);
		TypeFinder finder = new TypeFinder();
		finder.needed = type;
		root.accept(finder);
		return finder.result;
	}

	/**
	 * @return
	 */
	private List<Expression> extractInvariants(TypeDeclaration type) {
		if (type instanceof SpecTypeDeclaration) {
			SpecClause[] invs = ((SpecTypeDeclaration) type).getInvariants();
			if (invs == null || invs.length == 0)
				return Collections.emptyList();
			List<Expression> result = new ArrayList<Expression>(invs.length);
			for (SpecClause inv : invs)
				result.add(inv.getExpression());
			return result;
		} else {
			return Collections.emptyList();
		}
	}

	/**
	 * @author kevin
	 * @since Feb 13, 2011
	 */
	private static class JmlContractLookup implements Lookup {

		private final SpecMethodDeclaration decl;

		public JmlContractLookup(SpecMethodDeclaration decl) { this.decl = decl; }

		@Override
		public Field getField(Ref accessor, IVariableBinding field) {
			if (accessor == null)
				// FIXME resolve implicit this...
				accessor = new Local(Contract.THIS_VAR_NAME, field.getDeclaringClass());
			return new Field(accessor, field);
		}

		@Override
		public Ref getName(Expression e) {
			if (e instanceof SimpleName) {
				SimpleName name = (SimpleName) e;
				if ("\\result".equals(name.getIdentifier()))
					return new Local(Contract.RESULT_VAR_NAME, decl.resolveBinding().getReturnType());
				IVariableBinding var = (IVariableBinding) name.resolveBinding();
				if (var.isField())
					return getField(null, var);
				else if (var.isEnumConstant())
					return null;
//				else if (! var.isParameter())
//					throw new IllegalArgumentException("Cannot use local variable in contract: " + e);
				else
					return new Local(var);
			}
			if (e instanceof ThisExpression) {
				return new Local(e.toString(), ((ThisExpression) e).resolveTypeBinding());
			}
			throw new IllegalArgumentException("Not a variable: " + e);
		}

		@Override
		public Ref getSelect(Formula array, Formula index,
				ITypeBinding elementType) {
			if (array instanceof Pre) {
				Pre old = (Pre) array;
				if (0 < old.getArrayDim())
					throw new IllegalArgumentException("JML can directly encode old array cell contents");
			}
			return new Select(array, index, elementType);
		}
	}

	private static class TypeFinder extends ASTVisitor {

		ITypeBinding needed;
		TypeDeclaration result;

		@Override
		public boolean visit(TypeDeclaration node) {
			if (node.resolveBinding().equals(needed) || node.resolveBinding().getJavaElement().equals(needed.getJavaElement())) {
				if (result != null)
					throw new IllegalStateException("Type found twice: " + node);
				result = node;
				return false;
			}
			// catch anonymous inner classes...
			return true;
		}
	}
}
